T:Type, eq:EqDecider(T), as,bs:(T List), x:T.
(x  list-diff(eq; as; bs))  ((x  as)  ((x  bs))) 

latex

Definitions	x:A. B(x), P  Q, P  Q, t  T, (x  l), A, P  Q, EqDecider(T)
Lemmas	list-diff-property, deq wf